es:ES, ff:FIFO, f2f+:F2F+-decls.
plus-ify{i:l}(es;ff;is_req  ;is_ack ;awaiting ;owes_ack )
 (sndr, rcvr:ff.C, a, b, e:E. (f2f+-pred(e,a) & f2f+-pred(e,b))  (a = b)) 

latex

Definitions

t  ...$L, e c e', P  Q, A c B, P  Q, P  Q, SQType(T), {T}, , t  T, P & Q, P  Q, x:A. B(x), e(e1,e2].P(e), (e <loc e'), a = b, x  {FDLNOr12445}, [e: i p j], x:A. B(x), False, A, f2f+-pred(e',e)

Lemmas

acks-between-reqs, loc-of-req-sender, ack-pred-req, es-causle wf, es-causl transitivity1, es-causl wf, es-causle transitivity, es-causl weakening, es-causle weakening locl, reqs-between-acks, assert-eq-id, Id wf, Id sq, loc-of-ack-sender, es-locl-total, fifoSender-one-one, req-pred-ack, f2f+-pred-field, event system wf, FIFO wf, F2F+-decls wf, fifoS wf, fifoR wf, f2f+Owes wf, f2f+Wait wf, f2f+Ack wf, f2f+Req wf, plus-ify wf, fifoC wf, es-E wf, f2f+-pred wf, f2f+-property